es:ES, e':E, P:({e:E| loc(e) = loc(e')  Id }Prop). ee'.P(e)  P(e') & (e<e'. P(e)) 

latex

Definitions	(e <loc e'), x(s), x:A. B(x), t  T, P  Q, E, Prop, P  Q, e  e' , b, False, A, P & Q, loc(e), Id, ES, P  Q, P  Q, e<e'. P(e), ee'.P(e), True, T
Lemmas	member wf, squash wf, true wf, es-le wf, es-locl wf, event system wf, es-le-loc, Id wf, es-loc wf, es-loc-pred, es-le-self, es-E wf